w:World.
FairFifo
 (i:Id, b, a:.
 (a  b)
  (t:. (a  t)  (t < b)  (isnull(a(i;t))))
  ((x,q. s(i;a).x(q + (b - a))) = (x.s(i;b).x)  x:Idvartype(i;x))) 

latex

Definitions

, t  T, x:AB(x), A  B, a < b, b, P  Q, x:A. B(x), Id, , vartype(i;x), s = t, FairFifo, World, {x:A| B(x)} , i  j , Void, False, A, #$n, -n, n+m, n - m, x.A(x), <a, b>, {T}, SQType(T), a(i;t), isnull(a), , s ~ t, s(i;t).x, r + s, f(a), P  Q, P & Q, x:A  B(x), P  Q, left + right, P  Q, Dec(P), , A c B, , A  B, , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y), x,y:A//B(x;y), Type, r - s, Atom$n, if b then t else f fi , let x,y = A in B(x;y), r * s, True, T

Lemmas

qadd inv assoc q, qmul one qrng, mon assoc q, squash wf, true wf, qadd ac 1 q, qadd assoc, qadd-add, qmul wf, qsub wf, int-rational, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, decidable lt, qadd comm q, mon ident q, w-vartype wf, qadd wf, int inc rationals, rationals wf, w-s wf, assert wf, w-isnull wf, w-a wf, le wf, nat sq, ge wf, nat properties, world wf, fair-fifo wf, Id wf, nat wf